| 1: | p(0) | → 0 | |
| 2: | p(s(X)) | → X | |
| 3: | leq(0,Y) | → true | |
| 4: | leq(s(X),0) | → false | |
| 5: | leq(s(X),s(Y)) | → leq(X,Y) | |
| 6: | if(true,X,Y) | → activate(X) | |
| 7: | if(false,X,Y) | → activate(Y) | |
| 8: | diff(X,Y) | → if(leq(X,Y),n__0,n__s(n__diff(n__p(X),Y))) | |
| 9: | 0 | → n__0 | |
| 10: | s(X) | → n__s(X) | |
| 11: | diff(X1,X2) | → n__diff(X1,X2) | |
| 12: | p(X) | → n__p(X) | |
| 13: | activate(n__0) | → 0 | |
| 14: | activate(n__s(X)) | → s(activate(X)) | |
| 15: | activate(n__diff(X1,X2)) | → diff(activate(X1),activate(X2)) | |
| 16: | activate(n__p(X)) | → p(activate(X)) | |
| 17: | activate(X) | → X | |
| 18: | LEQ(s(X),s(Y)) | → LEQ(X,Y) | |
| 19: | IF(true,X,Y) | → ACTIVATE(X) | |
| 20: | IF(false,X,Y) | → ACTIVATE(Y) | |
| 21: | DIFF(X,Y) | → IF(leq(X,Y),n__0,n__s(n__diff(n__p(X),Y))) | |
| 22: | DIFF(X,Y) | → LEQ(X,Y) | |
| 23: | ACTIVATE(n__0) | → 0# | |
| 24: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 25: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
| 26: | ACTIVATE(n__diff(X1,X2)) | → DIFF(activate(X1),activate(X2)) | |
| 27: | ACTIVATE(n__diff(X1,X2)) | → ACTIVATE(X1) | |
| 28: | ACTIVATE(n__diff(X1,X2)) | → ACTIVATE(X2) | |
| 29: | ACTIVATE(n__p(X)) | → P(activate(X)) | |
| 30: | ACTIVATE(n__p(X)) | → ACTIVATE(X) | |